1. Field of the Invention
The present invention generally relates to the design of logic circuits, and more particularly to a method of verifying a logic design through liveness checking.
2. Description of the Related Art
As electronic systems such as computers grow more complex with an ever greater number of interconnected devices, it becomes increasingly important to ensure that a system (or subsystem) design is going to work properly before proceeding with fabrication preparation. A variety of techniques can be performed to evaluate a design-under-test, including simulation, proof by theorem (formal verification), and model-checking. Model checking was developed to complement simulation-based verification. During model checking, an integrated circuit (IC) design to be verified is modeled as a finite state machine, and a design specification is formalized by writing temporal logic properties. The reachable states of the design are then traversed in order to verify the properties. In case the property fails, a counterexample is generated in the form of a sequence of states leading up to the failure.
Various attributes of a design can be checked during verification. One technique is known as liveness checking. Liveness checking refers to the verification of properties of a logic design which are used to assess whether it will “eventually” behave in a correct way, i.e., something good must eventually happen. For example, if verifying an arbiter, one may wish to check the property that “every request presented to the arbiter must eventually be granted”. Such properties are critical to establish in modern hardware designs given that Moore's law is now entailing complex multi-core on top of multi-execution unit systems, systems on a chip (SoC), and increasingly complicated communication fabrics. Failure to adhere to such liveness properties entails unacceptable system performances, if not system deadlock. Any counterexample to such a property must be of infinite length, i.e., showing a request which never receives a grant. This is often represented using a finite-length trace, where some suffix of that trace—denoted by the assertion of a specially added LOOP signal—starts with a particular state, and ends with the identical state about to be repeated. Semantically, this represents an infinite length counterexample since the suffix behavior where the loop is asserted may be repeated as many times as desired to witness the request-without-grant scenario.
Liveness checking is in contrast to safety checking. A safety property asserts that something bad never should happen. Liveness properties can be translated to safety properties through a known transformation which effectively doubles the state elements of that design, enabling the ability to sample the current state of the design and to later check for a repetition, thereby completing a loop (see “Liveness checking as safety checking” by Armin Biere et al., International Workshop on Formal Methods for Industrial Critical Systems, 2002).
Liveness checks often require the specification of “fairness” conditions which impose restrictions on the behavior during the loop which may be presented as a failure. For example, perhaps the arbiter under verification has a skewed priority scheme such that high priority requests always take priority over low priority requests. An infinite sequence of high-priority requests may thus starve out low-priority requests in a valid design. It thus may be required to prevent the reporting of failures where high-priority requests within the loop starve out low-priority requests. The de-assertion of high-priority requests may thus be specified as a fairness constraint. FIG. 1 depicts the behavior of bounded liveness counterexample 2. It has prefix followed by suffix, where the suffix contains all the conditions required for the bounded liveness failure. In this example the simulation sets a loop repeat bound of 4, so once the suffix end state reaches the same condition a fourth time, a failure is reported.